i:Id, ds:x:Id fp Type, da:k:Knd fp Type, A:ecl(ds;da), snd:msg-spec(ds;da),
upd:update-spec(ds;da), j:Id.
msg-spec-loc(snd;i)
 (R-has-loc(ecl-machine at i with state ecl

 (R-has-loc(A

 (R-has-loc(state variables ds

 (R-has-loc(actions da

 (R-has-loc(sends snd

 (R-has-loc(updates upd;j)
 (~
 (i = j) 

latex

Definitions

t  T, Void, x:A. B(x), Top, Knd, type List, x:AB(x), x:A. B(x), S  T, false, p  q, <a,b>, , s = t, true, Id, Prop, b, Type, A, b, P  Q, x:AB(x), P & Q, P  Q, Unit, left+right, x. t(x), a:A fp B(a), x.A(x), 2of(t), IdDeq, f(x)?z, 1of(t), Valtype(da;k), State(ds), , Atom$n, ecl(ds;da), msg-spec(ds;da), msg-spec-loc(snd;i), update-spec(ds;da), es realizer ind Rinit compseq tag def, es realizer ind Rplus compseq tag def, R-has-loc(R;i), let a,b,c,d,e,f,g = u in v(a;b;c;d;e;f;g), R-state-var-init(i;ds;da;x;T;v;ks;tr), ecl-trans-tuple{i:l}(ds;da), ecl-trans(x), ecl-machine1{$ecl:ut2}(i; ds; da; A), ecl-machine at i with state $eclAstate variables dsactions dasends sndupdates upd, {T}, SQType(T), s ~ t, a = b, source(l), IdLnk, msg-spec-links(snd), IdLnkDeq, remove-repeats(eq;L), (x  l), , False, True, P  Q, T, car.cdr, nil, p  q, reduce(f;k;as), if b t else f fi, P  Q, ecl-tags(l;snd), null(as), update-spec-vars(upd)

Lemmas

cons member, update-spec-vars wf, band wf, assert of null, null wf3, ecl-tags wf, bor wf, squash wf, true wf, lsrc wf, Id sq, bfalse wf, member-remove-repeats, l member wf, remove-repeats wf, IdLnk wf, idlnk-deq wf, msg-spec-links wf, bool sq, msg-spec-loc wf, update-spec wf, msg-spec wf, ecl wf, ecl-trans wf, ecl-trans-tuple wf, R-state-var-loc, ecl-machine2-loc, fpf-trivial-subtype-top, nat wf, decl-state wf, ma-valtype wf, pi1 wf, fpf-cap wf, id-deq wf, pi2 wf, fpf wf, eqtt to assert, eqff to assert, iff transitivity, assert of bnot, not functionality wrt iff, assert-eq-id, bnot wf, not wf, assert wf, Id wf, eq id wf, bool wf, btrue wf, ecl-machine3-loc, top wf, Knd wf